Research Program
Application Domains
New Software and Platforms
New Results
- Hol-Light and Elpi
- Generating equality tests for inductive types
- Re-designing the state machine of Coq
- Formal proofs on session types
- Formal proofs of an axiomatization of graphs with tree-width two
- Formal study of double-word arithmetic algorithms
- Approximations using Chebyshev polynomials
- Formalizing computational analysis
- Formal study of probabilistic programs
- Security of a key management service
- High-assurance and high-speed SHA-3
- A domain-specific language for timing sensitive computation
- Proving equivalence between probabilistic programs
- MaskVerif: automated verification of higher-order masking in presence of physical defaults
- Frame type theory
- Automated refinements on algorithms in Lean
- Parametricity in Template Coq
- A hierarchy builder
- Adding measure theory to mathematical components analysis
- A formal description of exact real arithmetic
- Formal study of a triangulation algorithm
- Formal study of Voronoi diagrams and Fortune's algorithm
- Formal study of a cell-decomposition algorithm
- A guide to use Coq for security evaluations
- Formalization of the Poincaré disk model in Isabelle
- Integration of the GeoCoq library to Logipedia
- Performance improvements for a reflective tactic in the GeoCoq library
- Mutual interpretability of cartesian planes with Tarski's system of geometry
- Simplification of a constructive version of Tarski's system of geometry
- Formal proofs of Tarjan's strongly connected components algorithm
Partnerships and Cooperations
Bibliography
Research Program
Application Domains
New Software and Platforms
New Results
- Hol-Light and Elpi
- Generating equality tests for inductive types
- Re-designing the state machine of Coq
- Formal proofs on session types
- Formal proofs of an axiomatization of graphs with tree-width two
- Formal study of double-word arithmetic algorithms
- Approximations using Chebyshev polynomials
- Formalizing computational analysis
- Formal study of probabilistic programs
- Security of a key management service
- High-assurance and high-speed SHA-3
- A domain-specific language for timing sensitive computation
- Proving equivalence between probabilistic programs
- MaskVerif: automated verification of higher-order masking in presence of physical defaults
- Frame type theory
- Automated refinements on algorithms in Lean
- Parametricity in Template Coq
- A hierarchy builder
- Adding measure theory to mathematical components analysis
- A formal description of exact real arithmetic
- Formal study of a triangulation algorithm
- Formal study of Voronoi diagrams and Fortune's algorithm
- Formal study of a cell-decomposition algorithm
- A guide to use Coq for security evaluations
- Formalization of the Poincaré disk model in Isabelle
- Integration of the GeoCoq library to Logipedia
- Performance improvements for a reflective tactic in the GeoCoq library
- Mutual interpretability of cartesian planes with Tarski's system of geometry
- Simplification of a constructive version of Tarski's system of geometry
- Formal proofs of Tarjan's strongly connected components algorithm
Partnerships and Cooperations
Bibliography
Previous | 
Home